| Definitions | P   Q,  x:A. B(x), prop{i:l}, t  T, guard(T), False,  A, A  B,  x:A. B(x), P  Q, P  Q,  ,   x. t(x), A c B, ma-valtype(da; k), event-info(ds;da), e(e1,e2].P(e), True,  T, subtype(S; T), (x l),  , l_all(L; T; x.P(x)), e[e1,e2).P(e), star-append(T; P; Q), lelt(i; j; k), int_seg(i; j), suptype(S; T), es-le(es; e; e'), ff, tt, if b then t else f fi , Y, upto(n), es-hist{i:l}(es;e1;e2), top, reduce(f; k; as), concat(ll), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ||as||, P  Q, P Q, sq_type(T), x(s), es-locl(es; e; e'), e[e1,e2].P(e), Unit,  , decidable(P), null(as),  b, append(as; bs),  |
| Lemmas | es-loc wf, es-hist wf, ecl-es-act wf, iff wf, ecl-act wf, le wf, ecl-halt wf, append wf, event-info wf, top wf, Kind-deq wf, fpf-cap wf, decl-state wf, es-loc-pred, es-le-loc, es-locl-iff, es-pred wf, es-valtype wf, ecl-es-halt-ecl-halt, es-hist-partition, nat wf, ecl-es-halt wf, es-first wf, assert wf, not wf, existse-between3 wf, es-hist-is-append, ecl-halt-nil, ecl-act-nil, nat plus wf, iseg wf, ecl-ex wf, cons member, nat plus inc, ecl-halt-ex, alle-between1 wf, select wf, length wf1, l-all-iff, iseg-es-hist, l-all wf, l member wf, es-le wf, es-locl wf, non neg length, es-le weakening, es-hist-iseg, es-locl irreflexivity, es-le weakening eq, es-locl transitivity2, es-locl transitivity1, es-hist-one-one, upto wf, int seg wf, map wf, es-E wf, false wf, member map, es-vartype wf, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, assert of eq int, eqtt to assert, iff transitivity, bool wf, eq int wf, concat wf, append assoc sq, es-interval wf, append-nil, l all wf2, null wf3, decidable assert, decidable es-le, es-le-not-locl, decidable es-locl, null-es-hist, assert of null, es-hist-is-concat, Id sq, select member, length wf nat, bool sq, bool cases |
